import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes
import ProcessQueue
import ProcessDescr
import Lock

class ProcessTable(simsym.tstruct(
		procs		= symtypes.tdict(ptypes.IPREF, ProcessDescr.ProcessDescr),
		known_procs	= symtypes.tset(ptypes.IPREF),
		freeids		= symtypes.tset(ptypes.APREF)
		#size		= simsym.SInt
		)):
	def _declare_assumptions(self, assume):
		super(ProcessTable, self)._declare_assumptions(assume)
	
	@model.methodwrap()
	def INIT(self):
		#self.size = 0
		x = ptypes.IPREF.var("x")
		simsym.assume(simsym.forall(x, simsym.implies(
			self.known_procs.contains(x), x == ptypes.IdleProcRef
		)))

		y = ptypes.APREF.var("y")
		simsym.assume(simsym.forall(y, simsym.symeq(
			self.freeids.contains(y), simsym.symand(
				[y >= 1, y < ptypes.maxprocs])
		)))
		self.CreateIdleProcess
	
	@model.methodwrap()
	def CreateIdleProcess(self):
		#size = size + 1
		ipd = ProcessDescr.ProcessDescr.var("ipd")
		e = ptypes.PCODE.var("e")
		e.p = 0
		e.size = 0

		e2 = ptypes.PDATA.var("e2")
		e2.p = 0
		e2.size = 0

		e3 = ptypes.MEMDESC.var("e3")
		e3.p = 0
		e3.size = 0

		stkdesc = ptypes.PSTACK.var("stkdesc")
		stkdesc.p = 0
		stkdesc.size = 20

		pr = ptypes.PRIO.var("pr")
		memsz = simsym.SInt.var("memsz")

		ipd.INIT(pr, ptypes.pstready, stkdesc, e2, e, e3, memsz)
		self.procs[ptypes.IdleProcRef] = ipd
	@model.methodwrap(pid = ptypes.IPREF,
			  pd = ProcessDescr.ProcessDescr)
	def AddProcess(self, pid, pd):
		self.procs[pid] = pd
	
	@model.methodwrap(pid = ptypes.IPREF)
	def DelProcess(self, pid):
		return		    # XXX don't know why commuter forbids del
		del self.procs._map[pid] # does not matter if we don't really delete

	@model.methodwrap(pid = ptypes.IPREF)
	def DescrOfProcess(self, pid):
		#simsym.assume(self.procs.contains(pid))
		return self.procs._map[pid]
model_class = ProcessTable
